\begin{tabbing}
pre{-}init1{-}p(${\it es}$;$i$;$x$;$X$;$x_{0}$;$a$;$p$;$P$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\uparrow$($P$($x_{0}$))) $\Rightarrow$ ($\exists$$e$:E. (loc($e$) = $i$)))\+
\\[0ex]\& (\=(vartype($i$;$x$) $\subseteq$r $X$)\+
\\[0ex]c$\wedge$ \=($\forall$$e$@$i$. (kind($e$) = locl($a$)) $\Rightarrow$ ((valtype($e$) $\subseteq$r Outcome) c$\wedge$ ($\uparrow$($P$($x$ when $e$))))\+
\\[0ex]\& $\forall$$e$@$i$. $\exists$${\it e'}$$\geq$$e$.(kind(${\it e'}$) = locl($a$)) $\vee$ ($\neg$($\uparrow$($P$(($x$ after ${\it e'}$)))))))
\-\-\\[0ex]\& @$i$ $x$ initially $x_{0}$:$X$
\-
\end{tabbing}